Nuprl Definition : manames-overlap-case
11,40
postcript
pdf
if
nms1
and
nms2
overlap then
x
else
y
fi
== if
p
:l_disjoint(MaName;
nms1
;
nms2
) then
y
else
x
fi
latex
clarification:
if
nms1
and
nms2
overlap then
x
else
y
fi
== branch(l_disjoint(MaName;
nms1
;
nms2
);TERMOF{
decidable
l
disjoint
manames
:ObjectId, 1:l}
== branch(l_disjoint(MaName;
nms1
;
nms2
);
(
nms1
== branch(l_disjoint(MaName;
nms1
;
nms2
);
,
nms2
);
p
.
y
;
x
)
latex
Definitions
if
p
:
P
then
A
(
p
) else
B
fi
,
l_disjoint(
T
;
l1
;
l2
)
,
MaName
,
f
(
a
)
,
decidable
l
disjoint
manames
FDL editor aliases
manames-overlap-case
origin